k:, P:((k+1)).
search(k+1;P) = if P(0) 1 ; 0<search(k;i.P(i+1)) search(k;i.P(i+1))+1 else 0 fi   

latex

Definitions	AB, A, False, P  Q, search(k;P), if b t else f fi, {i..j}, x:A. B(x), , t  T, , Unit, P  Q, i  j < k, P & Q, Prop, b, P  Q, b, x:A. B(x), Dec(P), P  Q, T, i<j, ij, True, SQType(T), {T}, S  T
Lemmas	decidable lt, le int wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, assert of lt int, search wf, decidable int equal, assert wf, not wf, bnot wf, le wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, search property, nat wf, bool wf, int seg wf